FIncr  Type 

latex

ProofTree

Definitions	FIncr, t  T, True, {T}, x(s), P  Q, , x:A. B(x), WellFnd{i}(A;x,y.R(x;y)), T, , False, A, A  B, i  j , ff, tt, if b then t else f fi , x f y, P  Q, {i...}, a  b  T
Lemmas	nat wf, le wf, ge wf, nat properties, eq int eq false elim sqequal, eq int eq true elim sqequal, bool cases sqequal, eq int wf, int upper wf